philosophyfandomcom-20200223-history
First-order logic
First-order logic, also known as quantification theory and predicate calculus is a term that refers to predicate logics in which quantified predicates may range over a single domain of discourse that contains distinct objects. There are several first order logics, but the most commonly studied is classical first-order logic, which is supposed to be an "extension" of Propositional logic. Syntax Alphabet Logical symbols: *The Quantifiers: \forall, \exists . Respectively, the Universal Quantifier and the Existential Quantifier. *The logical connectives: \and, \or, \lnot, \rightarrow, \leftrightarrow Respectively, Conjunction, Disjunction, Material conditional, biconditional. Other logical connectives may also be added. *A set of infinite variables: x_1,x_2,x_3,\ldots . They may be identified with letters such as x,y,z . *A set of parentheses and other punctuation marks. Non-logical symbols *For every integer n, there is a set of n-ary Predicate symbols: P_1,P_2,P_3,\ldots . These may be letters such as A,B,C,D,\ldots,Y,Z *For every integer n, there is a set of n-ary function symbols.: f_1,f_2,f_3,\ldots . If the arity of these symbols is equal to 0, then it is said to be an individual constant. These may be letters such as a,b,c,d,\ldots,t,u,v,w Formation rules Terms: The set of terms is defined as: *Any expression f(t_1,t_2,t_3,\ldots,t_n) of n arguments (where t_n is a term and f is a function symbol) is a term. *Individual constants are terms. *Any variable is a term. Formulas *'Predicates:' If P is an n-ary predicate symbols, and t_1,t_2,t_3,\ldots,t_n are terms, then P(t_1,t_2,t_3,\ldots,t_n) is a wff (wff ''is an abbrevation for a well-formed formula ). *'Quantifiers': If \phi is a wff and x is a variable, then \forall x\phi and \exists x \phi are wffs. *'Negation': If \phi is a wff then \lnot \phi is a wff. *'Binary connectives': If \phi and \psi are wffs and \Box is a binary connective, then \phi \Box \psi is a wff. *'Equality Symbol': if equality is a part of first-order logic and \phi and \psi are wffs, then \phi = \psi is a wff. Semantics The non-logical symbols of a first-order logic are usually interpreted with a first-order model, which is an ordered pair \mathcal A = (A, \sigma, I). Where A is the domain of discourse, \sigma is the ''signature, and I is the interpretation function which assigns meaning to the non-logical symbols. The signature is an ordered pair \sigma = (\sigma_f,\sigma_r,ar) where \sigma_r is the set of predicate or relation symbols, \sigma_f is the set of function symbols, and ar is a mapping ar:\sigma_r \cup \sigma_f \to \mathbb N which assigns a natural number called an arity. The notation for an interpretation of a non-logical symbol x is I(x)=x^\mathcal A. Each predicate symbol or relation symbol R is assigned a n-ary relation R^\mathcal A\subseteq A^n or equivalently an n-ary function R^\mathcal A:D^n \to \mathbb B (where \mathbb B is the boolean domain or some other truth set). Each function symbol f is assigned an n-ary function f^\mathcal A :D^n \to D . If f is a nullary function (that is an individual constant) its interpretation is f^\mathcal A \in D . Individual constants may be assigned a value, such as f^\mathcal A = 100 . The semantics for a first-order logic could be defined inductively in the following way: *A logical connective is given a truth value based on it's truth function or truth table, just as in Propostional logic. *Let v_1, \ldots, v_n be the evaluations of the terms t_1, \ldots, t_n . Then P(t_1, \ldots, t_n) is true if and only if (v_1, \ldots, v_n) \in P^\mathcal{A} . (Function symbols are evalauted in the following way: Given terms t_1, \ldots t_n that have been evaulated to d_1,\ldots,d_n , the n-ary function value f(t_1,\ldots,t_n) evaulates to f^\mathcal{A}(d_1,\ldots,d_n) . * t_1=t_2 is true if and only if t_1 and t_2 evaulate to the same x \in D * \forall x \phi (x) is true if and only if \phi (x) for all x \in D . * \exists x \phi (x) is true if and only if there exists x \in D such that \phi (x) . Rules of inference The rules of inference for first-order logic depends on what formal system is being used. It is common to add the rules of inference of propositional logic, universal instantiation, universal generalization, existential instantiation, and existential generalization. Formal systems may also include Change of quantifier. Axioms If equality is part of a first-order logic system, then reflexivity, substitution for formulas, and substitution for functions are added as axioms. Symmetry and transitivity of equality follow from those three.